Lean is a strict , pure , functional , and dependent type language.
lean-lang.org
“
Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover. Lean programming primarily involves defining types and functions. This allows your focus to remain on the problem domain and manipulating its data, rather than the details of programming.
목차
Memo
bool과 Bool의 차이? (AnswerMe )=과 ==의 차이는?
Articles
목차 관련 글 When to annotate type 이 글을 인용: “아마도 Lean은 증명 언어이고 타입 시스템이 특히 복잡하기 때문(dependent type)인 것 같다.” Inductive type 관련 절: 프로그래밍 언어 예시 Why functional programming matters “Functional languages push those limits back.” 프로그래밍 패러다임 “In turn, a functional programming language is one that supports and encourages the functional style….” 자연어 기반 AI-인간 인터렉션의 한계 이 글을 인용: “인간-기계가 소통하기 위한, 배우긴 어렵지만 쓰긴 쉬운 언어.” Type-driven development 관련 절: Type-Driven Development with Idris 크리스토퍼 알렉산더가 소프트웨어 분야에 미친 영향 “"Our initial success using a pattern language for user interface design has left us quite enthusiastic about th…” Test and type-driven development 이 글을 인용: “예를 들어 Lean과 같이 의존 타입을 쓰는 언어에서는 코드의 상당 부분에 대해서 (원한다면) 동작의 무결성을 정적으로 검증할 수 있다.” Denotational semantics “This turned out to be an important observation that not only gave denotational semantics a new lease on life an…” 정적 프로그램과 동적 프로세스 관련 절: AOP AI 시대의 프로그래밍 교육 “실제로 프로그래밍 교육은 수학적 추론, 창의적 문제 해결 등 일부 인지적 능력을 향상시키는 전이 효과가 있다.” Software aspects of strategic defense systems 이 글을 인용: “당시에 아직 컴퓨팅 파워가 턱없이 부족하다고 평가했던 프로그램 검증은 이제 충분히 실용적으로 쓸 수 있는 기술이 되었다.” 프로그래밍은 비인간적이다 “새로운 편집기, 새로운 프로그래밍 언어, 새로운 운영체제, 새로운 기술도메인, 새로운 업무 도메인에서 개발해보기.” LeanTool 이 글을 인용: “"LeanTool: Helping LLMs Be Better at Lean"” 패턴 언어 관련 절: Christopher Alexander's pattern language AI 지원 프로그래밍을 위한 새 실천법 “But when I change the system, there is a human involved, and humans do care. --p4” 내가 읽은 책들 “Harnessed: how language and music mimicked nature and transformed ape to man” History of programming languages “표준 라이브러리: ALGOL 58, BASIC 등 초기 언어들은 표준 함수의 이름들이 예약어(keywords)였고 언어 구현과 표준 라이브러리를 구분하지 않았다.” The cognitive benefits of learning computer programming: A meta-analysis of transfer effects “Does computer programming teach students how to think?” 애스펙트 지향 프로그래밍 “OOP is a popular programming language technology.”